A:Type, B:(AType), eq:EqDecider(A), f1, g, f2:a:A fp B(a). f1  g  f2  g  f1  f2  g 

latex

Definitions	t  T, f(a), x(s), x:A. B(x), x. t(x), f  g, P  Q, a:A fp B(a), x:AB(x), EqDecider(T), Type, x.A(x), <a,b>, f  g, s = t, P  Q, x:AB(x), P & Q, P  Q, f || g, A & B, b, Top, x  dom(f), Prop, f(x)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-join-idempotent, fpf-join wf, fpf-join-sub, deq wf, fpf wf, fpf-sub wf